Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
U71(tt, L, N) → U72(isNat(N), L)
U72(tt, L) → s(length(L))
U81(tt) → nil
U91(tt, IL, M, N) → U92(isNat(M), IL, M, N)
U92(tt, IL, M, N) → U93(isNat(N), IL, M, N)
U93(tt, IL, M, N) → cons(N, take(M, IL))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U71(isNatList(L), L, N)
take(0, IL) → U81(isNatIList(IL))
take(s(M), cons(N, IL)) → U91(isNatIList(IL), IL, M, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U21: {1}
U31: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
U71: {1}
U72: {1}
isNat: empty set
s: {1}
length: {1}
U81: {1}
nil: empty set
U91: {1}
U92: {1}
U93: {1}
take: {1, 2}


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
U71(tt, L, N) → U72(isNat(N), L)
U72(tt, L) → s(length(L))
U81(tt) → nil
U91(tt, IL, M, N) → U92(isNat(M), IL, M, N)
U92(tt, IL, M, N) → U93(isNat(N), IL, M, N)
U93(tt, IL, M, N) → cons(N, take(M, IL))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U71(isNatList(L), L, N)
take(0, IL) → U81(isNatIList(IL))
take(s(M), cons(N, IL)) → U91(isNatIList(IL), IL, M, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U21: {1}
U31: {1}
U41: {1}
U42: {1}
isNatIList: empty set
U51: {1}
U52: {1}
isNatList: empty set
U61: {1}
U62: {1}
U71: {1}
U72: {1}
isNat: empty set
s: {1}
length: {1}
U81: {1}
nil: empty set
U91: {1}
U92: {1}
U93: {1}
take: {1, 2}

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, U62, s, length, U81, take, U421, U521, U621, LENGTH, U111, U211, U311, U811, TAKE} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U71, U72, U91, U92, U93, U411, U511, U611, U721, U711, U921, U911, U931} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATILIST, ISNATLIST, ISNAT, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

U411(tt, V2) → U421(isNatIList(V2))
U411(tt, V2) → ISNATILIST(V2)
U511(tt, V2) → U521(isNatList(V2))
U511(tt, V2) → ISNATLIST(V2)
U611(tt, V2) → U621(isNatIList(V2))
U611(tt, V2) → ISNATILIST(V2)
U711(tt, L, N) → U721(isNat(N), L)
U711(tt, L, N) → ISNAT(N)
U721(tt, L) → LENGTH(L)
U911(tt, IL, M, N) → U921(isNat(M), IL, M, N)
U911(tt, IL, M, N) → ISNAT(M)
U921(tt, IL, M, N) → U931(isNat(N), IL, M, N)
U921(tt, IL, M, N) → ISNAT(N)
ISNAT(length(V1)) → U111(isNatList(V1))
ISNAT(length(V1)) → ISNATLIST(V1)
ISNAT(s(V1)) → U211(isNat(V1))
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(V) → U311(isNatList(V))
ISNATILIST(V) → ISNATLIST(V)
ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(take(V1, V2)) → U611(isNat(V1), V2)
ISNATLIST(take(V1, V2)) → ISNAT(V1)
LENGTH(cons(N, L)) → U711(isNatList(L), L, N)
LENGTH(cons(N, L)) → ISNATLIST(L)
TAKE(0, IL) → U811(isNatIList(IL))
TAKE(0, IL) → ISNATILIST(IL)
TAKE(s(M), cons(N, IL)) → U911(isNatIList(IL), IL, M, N)
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)

The collapsing dependency pairs are DPc:

U721(tt, L) → L
U931(tt, IL, M, N) → N


The hidden terms of R are:

zeros
take(M, IL)

Every hiding context is built from:

take on positions {1, 2}

Hence, the new unhiding pairs DPu are :

U721(tt, L) → U(L)
U931(tt, IL, M, N) → U(N)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(zeros) → ZEROS
U(take(M, IL)) → TAKE(M, IL)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
U71(tt, L, N) → U72(isNat(N), L)
U72(tt, L) → s(length(L))
U81(tt) → nil
U91(tt, IL, M, N) → U92(isNat(M), IL, M, N)
U92(tt, IL, M, N) → U93(isNat(N), IL, M, N)
U93(tt, IL, M, N) → cons(N, take(M, IL))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U71(isNatList(L), L, N)
take(0, IL) → U81(isNatIList(IL))
take(s(M), cons(N, IL)) → U91(isNatIList(IL), IL, M, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 3 SCCs with 15 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, U62, s, length, U81, take} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U71, U72, U91, U92, U93, U511, U611, U411} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATLIST, ISNATILIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)
U511(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNATLIST(take(V1, V2)) → U611(isNat(V1), V2)
U611(tt, V2) → ISNATILIST(V2)
ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)
U411(tt, V2) → ISNATILIST(V2)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATLIST(take(V1, V2)) → ISNAT(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
U71(tt, L, N) → U72(isNat(N), L)
U72(tt, L) → s(length(L))
U81(tt) → nil
U91(tt, IL, M, N) → U92(isNat(M), IL, M, N)
U92(tt, IL, M, N) → U93(isNat(N), IL, M, N)
U93(tt, IL, M, N) → cons(N, take(M, IL))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U71(isNatList(L), L, N)
take(0, IL) → U81(isNatIList(IL))
take(s(M), cons(N, IL)) → U91(isNatIList(IL), IL, M, N)

Q is empty.

The following rules are not useable and can be deleted:

zeros → cons(0, zeros)
U71(tt, x0, x1) → U72(isNat(x1), x0)
U72(tt, x0) → s(length(x0))
U81(tt) → nil
U91(tt, x0, x1, x2) → U92(isNat(x1), x0, x1, x2)
U92(tt, x0, x1, x2) → U93(isNat(x2), x0, x1, x2)
U93(tt, x0, x1, x2) → cons(x2, take(x1, x0))
length(nil) → 0
length(cons(x0, x1)) → U71(isNatList(x1), x1, x0)
take(0, x0) → U81(isNatIList(x0))
take(s(x0), cons(x1, x2)) → U91(isNatIList(x2), x2, x0, x1)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52, take, U62, U31, U42} are replacing on all positions.
For all symbols f in {cons, U51, U61, U41, U511, U611, U411} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNATLIST, ISNATILIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)
U511(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNATLIST(take(V1, V2)) → U611(isNat(V1), V2)
U611(tt, V2) → ISNATILIST(V2)
ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)
U411(tt, V2) → ISNATILIST(V2)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(s(V1)) → ISNAT(V1)
ISNATLIST(take(V1, V2)) → ISNAT(V1)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
U61(tt, V2) → U62(isNatIList(V2))
isNatIList(V) → U31(isNatList(V))
U31(tt) → tt
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U62(tt) → tt
U52(tt) → tt
U11(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 1   
POL(ISNAT(x1)) = 2·x1   
POL(ISNATILIST(x1)) = 2·x1   
POL(ISNATLIST(x1)) = 2·x1   
POL(U11(x1)) = 0   
POL(U21(x1)) = 2·x1   
POL(U31(x1)) = 0   
POL(U41(x1, x2)) = 2 + 2·x1   
POL(U411(x1, x2)) = x1 + 2·x2   
POL(U42(x1)) = 0   
POL(U51(x1, x2)) = 2·x1   
POL(U511(x1, x2)) = 2·x1 + 2·x2   
POL(U52(x1)) = 2·x1   
POL(U61(x1, x2)) = 2·x1   
POL(U611(x1, x2)) = 2 + 2·x2   
POL(U62(x1)) = 0   
POL(cons(x1, x2)) = 2·x1 + x2   
POL(isNat(x1)) = 0   
POL(isNatIList(x1)) = 2   
POL(isNatList(x1)) = 0   
POL(length(x1)) = 2·x1   
POL(nil) = 2   
POL(s(x1)) = 2 + 2·x1   
POL(take(x1, x2)) = 2 + x1 + 2·x2   
POL(tt) = 0   
POL(zeros) = 2   

the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
U11(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U21(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNATLIST(take(V1, V2)) → U611(isNat(V1), V2)
U611(tt, V2) → ISNATILIST(V2)
ISNAT(s(V1)) → ISNAT(V1)
ISNATLIST(take(V1, V2)) → ISNAT(V1)

could be oriented strictly and thus removed.
The pairs

ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)
U511(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)
U411(tt, V2) → ISNATILIST(V2)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52, take, U62, U31, U42} are replacing on all positions.
For all symbols f in {cons, U51, U61, U41, U511, U411} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNATLIST, ISNATILIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(V) → ISNATLIST(V)
ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)
U511(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)
ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)
U411(tt, V2) → ISNATILIST(V2)
ISNATILIST(cons(V1, V2)) → ISNAT(V1)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
U61(tt, V2) → U62(isNatIList(V2))
isNatIList(V) → U31(isNatList(V))
U31(tt) → tt
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U62(tt) → tt
U52(tt) → tt
U11(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 2 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                          ↳ QCSDPReductionPairProof
                        ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52, take, U62, U31, U42} are replacing on all positions.
For all symbols f in {cons, U51, U61, U41, U511} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

U511(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
U61(tt, V2) → U62(isNatIList(V2))
isNatIList(V) → U31(isNatList(V))
U31(tt) → tt
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U62(tt) → tt
U52(tt) → tt
U11(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 2   
POL(ISNAT(x1)) = 1 + 2·x1   
POL(ISNATLIST(x1)) = 2·x1   
POL(U11(x1)) = 1   
POL(U21(x1)) = 1 + 2·x1   
POL(U31(x1)) = 0   
POL(U41(x1, x2)) = 1 + 2·x1   
POL(U42(x1)) = 1   
POL(U51(x1, x2)) = 0   
POL(U511(x1, x2)) = 2 + x1 + 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2)) = 0   
POL(U62(x1)) = 0   
POL(cons(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = 2·x1   
POL(isNatList(x1)) = 0   
POL(length(x1)) = 1 + x1   
POL(nil) = 1   
POL(s(x1)) = 1 + 2·x1   
POL(take(x1, x2)) = 2 + x1 + 2·x2   
POL(tt) = 0   
POL(zeros) = 2   

the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
U11(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U21(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

U511(tt, V2) → ISNATLIST(V2)
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
ISNAT(length(V1)) → ISNATLIST(V1)

could be oriented strictly and thus removed.
The pairs

ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                          ↳ QCSDPReductionPairProof
                            ↳ QCSDP
                              ↳ QCSDependencyGraphProof
                        ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52, take, U62, U31, U42} are replacing on all positions.
For all symbols f in {cons, U51, U61, U41, U511} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNATLIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → U511(isNat(V1), V2)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
U61(tt, V2) → U62(isNatIList(V2))
isNatIList(V) → U31(isNatList(V))
U31(tt) → tt
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U62(tt) → tt
U52(tt) → tt
U11(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                        ↳ QCSDP
                          ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52, take, U62, U31, U42} are replacing on all positions.
For all symbols f in {cons, U51, U61, U41, U411} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)
U411(tt, V2) → ISNATILIST(V2)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
U61(tt, V2) → U62(isNatIList(V2))
isNatIList(V) → U31(isNatList(V))
U31(tt) → tt
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U62(tt) → tt
U52(tt) → tt
U11(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 2   
POL(ISNATILIST(x1)) = 1 + x1   
POL(U11(x1)) = 0   
POL(U21(x1)) = 2·x1   
POL(U31(x1)) = 1   
POL(U41(x1, x2)) = 2 + 2·x2   
POL(U411(x1, x2)) = 2 + x1 + 2·x2   
POL(U42(x1)) = 0   
POL(U51(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U52(x1)) = 1 + x1   
POL(U61(x1, x2)) = 2 + 2·x1 + x2   
POL(U62(x1)) = 1   
POL(cons(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(isNat(x1)) = 0   
POL(isNatIList(x1)) = 2 + 2·x1   
POL(isNatList(x1)) = 2·x1   
POL(length(x1)) = 2 + x1   
POL(nil) = 2   
POL(s(x1)) = 2 + x1   
POL(take(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(tt) = 0   
POL(zeros) = 2   

the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
U11(tt) → tt
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U21(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

U411(tt, V2) → ISNATILIST(V2)

could be oriented strictly and thus removed.
The pairs

ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
                      ↳ AND
                        ↳ QCSDP
                        ↳ QCSDP
                          ↳ QCSDPReductionPairProof
                            ↳ QCSDP
                              ↳ QCSDependencyGraphProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {length, U11, s, U21, U52, take, U62, U31, U42} are replacing on all positions.
For all symbols f in {cons, U51, U61, U41, U411} we have µ(f) = {1}.
The symbols in {isNat, isNatList, isNatIList, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → U411(isNat(V1), V2)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
U61(tt, V2) → U62(isNatIList(V2))
isNatIList(V) → U31(isNatList(V))
U31(tt) → tt
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U62(tt) → tt
U52(tt) → tt
U11(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, U62, s, length, U81, take, TAKE} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U71, U72, U91, U92, U93, U921, U911, U931} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, U} are not replacing on any position.

The TRS P consists of the following rules:

U911(tt, IL, M, N) → U921(isNat(M), IL, M, N)
U921(tt, IL, M, N) → U931(isNat(N), IL, M, N)
U931(tt, IL, M, N) → U(N)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(take(M, IL)) → TAKE(M, IL)
TAKE(s(M), cons(N, IL)) → U911(isNatIList(IL), IL, M, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
U71(tt, L, N) → U72(isNat(N), L)
U72(tt, L) → s(length(L))
U81(tt) → nil
U91(tt, IL, M, N) → U92(isNat(M), IL, M, N)
U92(tt, IL, M, N) → U93(isNat(N), IL, M, N)
U93(tt, IL, M, N) → cons(N, take(M, IL))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U71(isNatList(L), L, N)
take(0, IL) → U81(isNatIList(IL))
take(s(M), cons(N, IL)) → U91(isNatIList(IL), IL, M, N)

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(take(M, IL)) → TAKE(M, IL)
TAKE(s(M), cons(N, IL)) → U911(isNatIList(IL), IL, M, N)
The remaining pairs can at least be oriented weakly.

U911(tt, IL, M, N) → U921(isNat(M), IL, M, N)
U921(tt, IL, M, N) → U931(isNat(N), IL, M, N)
U931(tt, IL, M, N) → U(N)
Used ordering: Combined order from the following AFS and order.
U921(x1, x2, x3, x4)  =  x4
U911(x1, x2, x3, x4)  =  x4
U931(x1, x2, x3, x4)  =  x4
U(x1)  =  x1
TAKE(x1, x2)  =  x2

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, U62, s, length, U81, take} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U71, U72, U91, U92, U93, U921, U911, U931} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, U} are not replacing on any position.

The TRS P consists of the following rules:

U911(tt, IL, M, N) → U921(isNat(M), IL, M, N)
U921(tt, IL, M, N) → U931(isNat(N), IL, M, N)
U931(tt, IL, M, N) → U(N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
U71(tt, L, N) → U72(isNat(N), L)
U72(tt, L) → s(length(L))
U81(tt) → nil
U91(tt, IL, M, N) → U92(isNat(M), IL, M, N)
U92(tt, IL, M, N) → U93(isNat(N), IL, M, N)
U93(tt, IL, M, N) → cons(N, take(M, IL))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U71(isNatList(L), L, N)
take(0, IL) → U81(isNatIList(IL))
take(s(M), cons(N, IL)) → U91(isNatIList(IL), IL, M, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 3 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, U62, s, length, U81, take, LENGTH} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U71, U72, U91, U92, U93, U721, U711} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

U711(tt, L, N) → U721(isNat(N), L)
U721(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → U711(isNatList(L), L, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
U71(tt, L, N) → U72(isNat(N), L)
U72(tt, L) → s(length(L))
U81(tt) → nil
U91(tt, IL, M, N) → U92(isNat(M), IL, M, N)
U92(tt, IL, M, N) → U93(isNat(N), IL, M, N)
U93(tt, IL, M, N) → cons(N, take(M, IL))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U71(isNatList(L), L, N)
take(0, IL) → U81(isNatIList(IL))
take(s(M), cons(N, IL)) → U91(isNatIList(IL), IL, M, N)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 2   
POL(LENGTH(x1)) = 2·x1   
POL(U11(x1)) = x1   
POL(U21(x1)) = 2·x1   
POL(U31(x1)) = 2   
POL(U41(x1, x2)) = 2   
POL(U42(x1)) = 2   
POL(U51(x1, x2)) = 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2)) = x1   
POL(U62(x1)) = x1   
POL(U71(x1, x2, x3)) = 2·x2   
POL(U711(x1, x2, x3)) = 2·x1 + 2·x2   
POL(U72(x1, x2)) = 2·x2   
POL(U721(x1, x2)) = 2·x2   
POL(U81(x1)) = 2   
POL(U91(x1, x2, x3, x4)) = 2·x2 + 2·x3   
POL(U92(x1, x2, x3, x4)) = 2·x2 + 2·x3   
POL(U93(x1, x2, x3, x4)) = 2·x2 + 2·x3   
POL(cons(x1, x2)) = 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = 2   
POL(isNatList(x1)) = x1   
POL(length(x1)) = x1   
POL(nil) = 2   
POL(s(x1)) = 2·x1   
POL(take(x1, x2)) = x1 + x2   
POL(tt) = 2   
POL(zeros) = 0   

the following usable rules

isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
length(nil) → 0
length(cons(N, L)) → U71(isNatList(L), L, N)
U71(tt, L, N) → U72(isNat(N), L)
U72(tt, L) → s(length(L))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
take(0, IL) → U81(isNatIList(IL))
take(s(M), cons(N, IL)) → U91(isNatIList(IL), IL, M, N)
U81(tt) → nil
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
U31(tt) → tt
zeros → cons(0, zeros)
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U91(tt, IL, M, N) → U92(isNat(M), IL, M, N)
U92(tt, IL, M, N) → U93(isNat(N), IL, M, N)
U93(tt, IL, M, N) → cons(N, take(M, IL))
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
U11(tt) → tt
U21(tt) → tt

could all be oriented weakly.
Furthermore, the pairs

U711(tt, L, N) → U721(isNat(N), L)

could be oriented strictly and thus removed.
The pairs

U721(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → U711(isNatList(L), L, N)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPReductionPairProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U11, U21, U31, U42, U52, U62, s, length, U81, take, LENGTH} are replacing on all positions.
For all symbols f in {cons, U41, U51, U61, U71, U72, U91, U92, U93, U721, U711} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

U721(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → U711(isNatList(L), L, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(V2))
U52(tt) → tt
U61(tt, V2) → U62(isNatIList(V2))
U62(tt) → tt
U71(tt, L, N) → U72(isNat(N), L)
U72(tt, L) → s(length(L))
U81(tt) → nil
U91(tt, IL, M, N) → U92(isNat(M), IL, M, N)
U92(tt, IL, M, N) → U93(isNat(N), IL, M, N)
U93(tt, IL, M, N) → cons(N, take(M, IL))
isNat(0) → tt
isNat(length(V1)) → U11(isNatList(V1))
isNat(s(V1)) → U21(isNat(V1))
isNatIList(V) → U31(isNatList(V))
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(isNat(V1), V2)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(isNat(V1), V2)
isNatList(take(V1, V2)) → U61(isNat(V1), V2)
length(nil) → 0
length(cons(N, L)) → U71(isNatList(L), L, N)
take(0, IL) → U81(isNatIList(IL))
take(s(M), cons(N, IL)) → U91(isNatIList(IL), IL, M, N)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 2 less nodes.